\input memo.tex[let,jmc]
Stanford University proposes research to be carried out by Professor
John McCarthy and a graduate student.  It will cost \$xxx for a
three year period including salaries, secretarial help, computer use
and equipment.

	The research involves three related areas.

	1. The declarative components of large systems, e.g. megaprograms,
and their interaction with the procedural components.  It will emphasize
representing facts about actions, e.g. procedural components, and
reasoning about them.

	2. Specification and verification of programs that interact with
the world.  It will emphasize the relation between the {\it illocutionary}
specifications that relate inputs to outputs and the {\it perlocutionary}
specifications concerning what the program accomplishes in the world.

	3. Programming and communication languages for components of
distributed systems in which other components belong to different
organizations, e.g. different companies.  The main vehicle for this
research will be specifying (but not implementing) the Elephant 2000
programming language that includes an input-output language whose
statements are ``speech acts'', e.g. questions, answers, requests,
promises and offers.  The specifications of Elephant programs include
that questions are answered truthfully and responsively and that
promises are authorized and kept.

\noindent Discussion and motivation

Declarative components of systems (e.g. of megaprograms)

	Large systems, e.g. megaprograms, are built from components.
These components and their connection should meet the following
goals.

1. The interfaces between components are easier to understand and
specify than the detailed construction of the components themselves.

2. The components can be specified separately and built by people
with limited understanding of the other components.

3. When the system has to be changed, changes need only be made
in a few components (best only one) and a few of the interfaces.
The division into components was unsuccessful if revision
in specifications requires a substantial revision of this
division.

	When we consider how people think about systems and
how they think about modifying them, we see that many of the
components are declarative in character, i.e. consist of bodies
of facts that the system takes into account.  Moreover,
many of the modifications people need to make in systems
are initially thought of as taking new facts into account.
To the extent that components have a declarative structure,
desired modifications will take the form of modifying only
one or a few components.


\noindent Illocutionary and Perlocutionary Specifications

	A program that interacts with the world can have two kinds
of specifications, which we call illocutionary and perlocutionary
in a generalization of the corresponding terms for speech acts
as studied by philosophers.  Requesting or commanding that a
person do something is called illocutionary, whereas actually
getting him to do it is perlocutionary.

	Illocutionary specifications relate the inputs and outputs of
a program.  They can be verified by someone who understands the
program and the programming language.  Suitably axiomatizing the
language makes possible computer checkable formal proofs that programs
meet their illocutionary specifications.

	Perlocutionary specifications specify what the program
accomplishes in the world.  Their statement requires a language in
which facts about the relevant aspects of the world can be stated.
Their verification must be based on assumptions about what information
the program obtains about the world and the effects of the programs
actions.  If this verification is to be formal, then the relevant
facts must be expressed as axioms.

	These ideas about illocutionary and perlocutionary specifications
were originated in connection with the Elephant 2000 programming
language that is the subject of the next section.  However, they
are actually applicable to programs that interact with the
outside world no matter what the programming language is.

	Therefore, we plan to develop these forms of specification
outside of Elephant as well as inside it.


\noindent
Elephant 2000: A Programming Language Based on Speech Acts

	The goals and status of the Elephant 2000 programming
language are more fully described in Appendix A.  Here we
include only an abstract.

\noindent Abstract: Elephant 2000 is a vehicle for some ideas about
programming language features.  We expect these features to be
valuable in writing and verifying programs that interact with
people (e.g. transaction processing) or interact with programs belonging
to other organizations (e.g. electronic data interchange)
\hfill\break 1. Communication inputs and outputs are in an I-O
language whose sentences are meaningful speech acts approximately
in the sense of philosophers and linguists.  These include
questions, answers, offers, acceptances, declinations, requests,
permissions and promises.
\hfill\break 2. The correctness of programs is partially defined in
terms of proper performance of the speech acts.  Answers should
be truthful and responsive, and promises should be kept.  Sentences of logic expressing
these forms of correctness can be generated automatically
from the form of the program.
\hfill\break 3. Elephant source programs may not need data
structures, because they can refer directly to the past.  Thus a
program can say that an airline passenger has a reservation if he
has made one and hasn't cancelled it.
\hfill\break 4. Elephant programs themselves will be represented as
sentences of logic.  Their properties follow from this
representation without an intervening theory of programming or
anything like Hoare axioms.
\hfill\break 5. Elephant programs that interact non-trivially with
the outside world can have both {\it illocutionary} and {\it perlocutionary}
specifications, i.e. behavioral specifications relating inputs and outputs,
and specifications concerning what they accomplish in the world.

\noindent
For more information contact jmc@cs.stanford.edu.

\noindent
This file is /u/jmc/s90/formal.pro on gang-of-four.stanford.edu.
\vfill\end